\begin{tabbing}
$\forall$$T$:Type. 
\\[0ex]subtype\_rel($T$; $\mathbb{Z}$)
\\[0ex]$\Rightarrow$ \=($\forall$${\it as}$:($T$ List). \+
\\[0ex](sorted(${\it as}$) $\wedge$ no\_repeats($T$; ${\it as}$))
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\forall$$i$:int\_seg(0; $\parallel$${\it as}$$\parallel$), $j$:int\_seg(0; $i$). ${\it as}$[$j$] $<$ ${\it as}$[$i$]))
\-
\end{tabbing}